\begin{tabbing}
ES
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$${\it pred?}$:($E$$\rightarrow$($E$+Unit))
\\[0ex]$\times$${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id))
\\[0ex]$\times$EOrderAxioms($E$; ${\it pred?}$; ${\it info}$)
\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$$V$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$${\it init}$:($i$,$x$:Id$\rightarrow$$T$($i$,$x$))
\\[0ex]$\times$${\it Trans}$:($i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($x$:Id$\rightarrow$\=$T$\+
\\[0ex]($i$
\\[0ex],$x$)))
\-\\[0ex]$\times$${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.$V$(loc($e$),$a$); $l$,$t$.$M$($l$,$t$) ))
\\[0ex]$\times$${\it Send}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) )$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$\+
\\[0ex](Msg($M$) List))
\-\\[0ex]$\times$${\it Choose}$:($i$,$a$:Id$\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$))$\rightarrow$($V$($i$,$a$)+Unit))
\\[0ex]$\times$val{-}axiom(\=$E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;${\it Choose}$;
\\[0ex]${\it Send}$;${\it val}$)
\-\\[0ex]$\times$(\=($\forall$$i$, $x$:Id. AtomFree(Type;$T$($i$,$x$)))\+
\\[0ex]\& ($\forall$$i$, $a$:Id. AtomFree(Type;$V$($i$,$a$)))
\\[0ex]\& ($\forall$$l$:IdLnk, ${\it tg}$:Id. AtomFree(Type;$M$($l$,${\it tg}$))))
\-\\[0ex]$\times$Top
\-
\end{tabbing}